Formal verification with KEVM
概要
KのReachability Logic proverをKEVMにおいて使い、EVMバイトコードを形式的に検証する
以下のモジュールの正しさが前提
KEVM
Kのreachability logic theorem prover
Z3
specification
人の頭の中にあるものをspecificationに落とし込むところで間違う・不足することがある
例: ERC20だと、「同じaddressにtransferする」というのは(形式的仕様としては)別のケースとして扱わなければならない(成功ケース, 失敗ケース, 同様にtransferFromでも同じ場合分けがある)が、公式の(非形式的な)仕様だと見落とされていた SolidityではなくEVMバイトコードのレベルで検証を行うべき理由
高級言語ごとに作る必要がない
スタックサイズの最大やガス計算など、高級言語レイヤーでは現れない重要な部分がある
コンパイラのバグの影響を受けない
→同様の理由で、「coqやIsabelleでコントラクトを書いてEVMバイトコードにコンパイル」という方向性は微妙
参考
シンプルな足し算の関数のオーバーフローなどの検証の解説動画 YouTube 具体的な方法
検証対象のEVMバイトコードを、KEVMのセマンティックの通りにシンボリック実行していく
同じく、検証したいspecificationの通りに実行していく
ステートの扱い
外部のコントラクトを呼ぶ場合はあらかじめ入れておく必要がある？
EVM特有の工夫
EVM固有の困難と、現実的にSMTソルバで扱えるようにするためのabstraction & lemma
特にバイト操作演算は整数の非線形演算を必要とし、一般的に非決定可能
Resources
Abstractions for local memory
EVMではメモリのみが1byte単位、スタックとストレージは32byte単位
課題: mload/mstoreの際、バイト列をmerge/splitする必要があり、これが非線形演算になる
merge: $ x_nを、バイト列における(対応する桁数が小さい方から数えた時の)インデックスnのバイトだとすると、
https://gyazo.com/bef19ca4ab28523c2b8079c0ef09381f
上記のような$ mergeに関して、SMTソルバは$ x = {merge}(x_{31}, \cdots, x_0)を解こうとしてしまい、タイムアウトする
そこで、ワードレベルでの推論を可能にするべく、mload/mstoreのシンボリック実行に置いてメモリの抽象化を行う
Arithmetic Overflow
EVMの算術におけるオーバーフローのチェックには標準がなく、コンパイラ・ライブラリごとに違う
例えば、Vyperでは$ a+bは$ b == 0 || a + b > aとしてチェックされる
しかし、$ a+b < 2^{256}の方がシンプルそうだが、これと同値であることを示そうとするとZ3はタイムアウトする
Abstraction for hash
ハッシュ計算のアルゴリズムを毎回厳密に考慮するのは現実的ではない(そもそも一方向なので。。。)
SHA3はcollision freeではないと言う問題がある
下記で使われる
関数シグネチャ
可変長配列のストレージスロット
マッピング型のストレージスロット(本来のslotポジション(p)はゼロのままでhash(key, p)の位置)
安直にハッシュ関数を単射の関数で抽象化するのではなく、シンボリック実行時に(そのコンテキストにおいて)単射の性質を持つよう初期化する
pirapiraさんの方でも、SolidityのArray accessにおけるkeccakで単射を仮定していた(参考) Arithmetic Simplification Rules
算術を簡略化するrules
例:$ (x \times y)~/~y = x , ~{if}~ y \neq 0
例: , 0xff · · · f & n
https://gyazo.com/ed5bd87be6efb81ad0300a91338f3295
外部関数のコール
Uniswapの検証において、外部関数のコールを抽象化している
具体例
ERC20
具体的にいくつかのERC20トークン実装に関してRuntime Verificationが行った検証
ERC20の仕様自体は厳密なプロパティを定義しているわけではない(例えば、オーバーフローさせないことなどはある意味当然ながら言及されていない)ので、検証したプロパティは独自のもの
実際にバグがあったHKGはしっかりとオーバーフローなどの問題が検知された
Vyper ERC20は問題なかったらしい
Casper FFG contractの形式的検証
Runtime Verificationがgrant採択された時のメインスコープ
スマートコントラクト部分のみ、ネットワークレベル(delaying the contract, initializing epochs, fork choice rule.)の正当性を前提とした検証
k-dss: MakerDAOのMulti collateral daiの形式的検証
複数種類のコラテラルの仕組みを実装したDSS(Dai Stablecoin Simulation)GitHub Repoの形式的検証 Dapphub
これ元にout/spec以下に生成された.kファイルがある
この時点で形式的検証専門で3人の研究者がいたらしい
Resources
他の実用例
verified-smart-contractsリポジトリ
Casper FFGのコントラクトや、各種ERC20トークンコントラクトなど。VyperのERC20も検証されている
ERC20-K
ハイレベルに書かれていて、EVMレベルのことが書かれていない。verified-smart-contractsリポジトリのERC20 specの方が新しい。
命令型言語IMPでテスト書いている
eDSL
KのReachability logic theorem proverをKEVMで使うときの、specification定義用のDSL GitHub file Runtime Verificationのverified-smart-contractsリポジトリで使われている
手順に書いてある通りにすると、テンプレートと設定ファイルを元にspec/以下に.kのspecファイルが作られる MakerDAOのk-dssでも使われている
テンプレート&ハイレベル表記法
KEVMのconfigurationsに関するReachabilit Claim
パラメタをiniファイルの形式で設定して使う
verified-smat-contracts Repoだとこれ ABI Call Data, ABI Event Log, Hashed Location for Storage(ストレージのKey)に関してはハイレベルな表記法がある